g, h:IGroup, f:MonHom(g,h), a:|g|. f(~(a)) = ~(f(a))  |h| 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup, MonHom(M1,M2)
Definitions	t  T, x:A. B(x), P  Q, P & Q, P  Q, P  Q, x f y, IMonoid, IGroup, MonHom(M1,M2)
Lemmas	igrp wf, monoid hom wf, grp car wf, grp inv wf, grp eq op l, grp id wf, monoid hom id, grp inverse, grp op wf, monoid hom op